$\forall$$T$, ${\it T'}$:Type\{i\}, $L$:($T$ List), $f$:(\{$x$:$T$$\mid$ ($x$ $\in$ $L$)\} $\rightarrow$${\it T'}$), $P$:(${\it T'}$$\rightarrow$${\it T'}$$\rightarrow\mathbb{P}$\{i'\}).
\\[0ex]($\forall$$x$, $y$:$T$. ($x$ $\in$ $L$) $\Rightarrow$ ($y$ $\in$ $L$) $\Rightarrow$ $P$($f$($x$),$f$($y$))) $\Rightarrow$ ($\forall$$x$,$y$$\in$mapl($f$;$L$).  $P$($x$,$y$))